es:ES, e:E.
((first(e)))
 ((timed)state after pred(e)+time(e) - time(pred(e))
 (=
 (es_state_when(es;e)
 ( es_state(es;loc(e))) 

latex

Definitions

let x = a in b(x), f(a), EState(T), x:A  B(x), pred(e), when-after(e;info;pred?;init;Trans;val;time), t.2, s+r, <a, b>, t.1, Id, , x:AB(x), s = t, x:A. B(x), t  T, b, A, b, , , False, P  Q, first(e), P & Q, P  Q, Unit, left + right, es-T(es), es_time(es), es_val(es), es-Trans(es), es_init(es), es-pred?(es), es_info(es), es_vartype(es;i;x), es_state_when(es;e), time(e), pred(e), (timed)state after e, es_state(es;i), loc(e), first(e), E, ES, {T}, SQType(T), r - s, A c B, EOrderAxioms(E; pred?; info), loc(e), s ~ t

Lemmas

when-after wf, es-shift wf, qsub wf, pred wf, Id sq, subtype rel self, EState wf, loc wf, Id wf, event system wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, first wf, bool wf, bnot wf, not wf, assert wf